P:(chain_master()).
(list:(Id List). P(cmconfig(list)))
 (from, to:Id, num:. P(cmseq(from;to;num)))
 {x:chain_master(). P(x)} 

latex

Definitions	t  T, {T}, x(s), P  Q, , x:A. B(x), cmseq(from;to;num), cmconfig(list), chain_master()
Lemmas	cmconfig wf, cmseq wf, nat wf, Id wf, chain master wf